0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 198 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 1 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 PiDP
↳31 PiDPToQDPProof (⇒, 0 ms)
↳32 QDP
↳33 Narrowing (⇒, 0 ms)
↳34 QDP
↳35 UsableRulesProof (⇔, 0 ms)
↳36 QDP
↳37 QReductionProof (⇔, 0 ms)
↳38 QDP
↳39 QDPOrderProof (⇔, 52 ms)
↳40 QDP
↳41 DependencyGraphProof (⇔, 0 ms)
↳42 TRUE
↳43 PiDP
↳44 UsableRulesProof (⇔, 0 ms)
↳45 PiDP
↳46 PiDPToQDPProof (⇒, 0 ms)
↳47 QDP
↳48 QDPSizeChangeProof (⇔, 0 ms)
↳49 YES
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gaa(X, Y, Z))
sub_in_gaa(s(X), s(Y), Z) → U6_gaa(X, Y, Z, sub_in_gaa(X, Y, Z))
sub_in_gaa(X, 0, X) → sub_out_gaa(X, 0, X)
U6_gaa(X, Y, Z, sub_out_gaa(X, Y, Z)) → sub_out_gaa(s(X), s(Y), Z)
U2_gag(X, Y, R, sub_out_gaa(X, Y, Z)) → U3_gag(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, R) → U1_ggg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_ggg(X, Y, R, notZero_out_g(Y)) → U2_ggg(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_ggg(X, Y, R, sub_out_gga(X, Y, Z)) → U3_ggg(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, X) → U4_ggg(X, Y, notZero_in_g(Y))
U4_ggg(X, Y, notZero_out_g(Y)) → U5_ggg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_ggg(X, Y, geq_out_gg(X, Y)) → rem_out_ggg(X, Y, X)
U3_ggg(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_ggg(X, Y, R)
U3_gag(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_ga(X, Y))
geq_in_ga(s(X), s(Y)) → U7_ga(X, Y, geq_in_ga(X, Y))
geq_in_ga(X, 0) → geq_out_ga(X, 0)
U7_ga(X, Y, geq_out_ga(X, Y)) → geq_out_ga(s(X), s(Y))
U5_gag(X, Y, geq_out_ga(X, Y)) → rem_out_gag(X, Y, X)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gaa(X, Y, Z))
sub_in_gaa(s(X), s(Y), Z) → U6_gaa(X, Y, Z, sub_in_gaa(X, Y, Z))
sub_in_gaa(X, 0, X) → sub_out_gaa(X, 0, X)
U6_gaa(X, Y, Z, sub_out_gaa(X, Y, Z)) → sub_out_gaa(s(X), s(Y), Z)
U2_gag(X, Y, R, sub_out_gaa(X, Y, Z)) → U3_gag(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, R) → U1_ggg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_ggg(X, Y, R, notZero_out_g(Y)) → U2_ggg(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_ggg(X, Y, R, sub_out_gga(X, Y, Z)) → U3_ggg(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, X) → U4_ggg(X, Y, notZero_in_g(Y))
U4_ggg(X, Y, notZero_out_g(Y)) → U5_ggg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_ggg(X, Y, geq_out_gg(X, Y)) → rem_out_ggg(X, Y, X)
U3_ggg(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_ggg(X, Y, R)
U3_gag(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_ga(X, Y))
geq_in_ga(s(X), s(Y)) → U7_ga(X, Y, geq_in_ga(X, Y))
geq_in_ga(X, 0) → geq_out_ga(X, 0)
U7_ga(X, Y, geq_out_ga(X, Y)) → geq_out_ga(s(X), s(Y))
U5_gag(X, Y, geq_out_ga(X, Y)) → rem_out_gag(X, Y, X)
REM_IN_GAG(X, Y, R) → U1_GAG(X, Y, R, notZero_in_a(Y))
REM_IN_GAG(X, Y, R) → NOTZERO_IN_A(Y)
U1_GAG(X, Y, R, notZero_out_a(Y)) → U2_GAG(X, Y, R, sub_in_gaa(X, Y, Z))
U1_GAG(X, Y, R, notZero_out_a(Y)) → SUB_IN_GAA(X, Y, Z)
SUB_IN_GAA(s(X), s(Y), Z) → U6_GAA(X, Y, Z, sub_in_gaa(X, Y, Z))
SUB_IN_GAA(s(X), s(Y), Z) → SUB_IN_GAA(X, Y, Z)
U2_GAG(X, Y, R, sub_out_gaa(X, Y, Z)) → U3_GAG(X, Y, R, rem_in_ggg(Z, Y, R))
U2_GAG(X, Y, R, sub_out_gaa(X, Y, Z)) → REM_IN_GGG(Z, Y, R)
REM_IN_GGG(X, Y, R) → U1_GGG(X, Y, R, notZero_in_g(Y))
REM_IN_GGG(X, Y, R) → NOTZERO_IN_G(Y)
U1_GGG(X, Y, R, notZero_out_g(Y)) → U2_GGG(X, Y, R, sub_in_gga(X, Y, Z))
U1_GGG(X, Y, R, notZero_out_g(Y)) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, sub_in_gga(X, Y, Z))
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
U2_GGG(X, Y, R, sub_out_gga(X, Y, Z)) → U3_GGG(X, Y, R, rem_in_ggg(Z, Y, R))
U2_GGG(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGG(Z, Y, R)
REM_IN_GGG(X, Y, X) → U4_GGG(X, Y, notZero_in_g(Y))
REM_IN_GGG(X, Y, X) → NOTZERO_IN_G(Y)
U4_GGG(X, Y, notZero_out_g(Y)) → U5_GGG(X, Y, geq_in_gg(X, Y))
U4_GGG(X, Y, notZero_out_g(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → U7_GG(X, Y, geq_in_gg(X, Y))
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
REM_IN_GAG(X, Y, X) → U4_GAG(X, Y, notZero_in_a(Y))
REM_IN_GAG(X, Y, X) → NOTZERO_IN_A(Y)
U4_GAG(X, Y, notZero_out_a(Y)) → U5_GAG(X, Y, geq_in_ga(X, Y))
U4_GAG(X, Y, notZero_out_a(Y)) → GEQ_IN_GA(X, Y)
GEQ_IN_GA(s(X), s(Y)) → U7_GA(X, Y, geq_in_ga(X, Y))
GEQ_IN_GA(s(X), s(Y)) → GEQ_IN_GA(X, Y)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gaa(X, Y, Z))
sub_in_gaa(s(X), s(Y), Z) → U6_gaa(X, Y, Z, sub_in_gaa(X, Y, Z))
sub_in_gaa(X, 0, X) → sub_out_gaa(X, 0, X)
U6_gaa(X, Y, Z, sub_out_gaa(X, Y, Z)) → sub_out_gaa(s(X), s(Y), Z)
U2_gag(X, Y, R, sub_out_gaa(X, Y, Z)) → U3_gag(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, R) → U1_ggg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_ggg(X, Y, R, notZero_out_g(Y)) → U2_ggg(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_ggg(X, Y, R, sub_out_gga(X, Y, Z)) → U3_ggg(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, X) → U4_ggg(X, Y, notZero_in_g(Y))
U4_ggg(X, Y, notZero_out_g(Y)) → U5_ggg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_ggg(X, Y, geq_out_gg(X, Y)) → rem_out_ggg(X, Y, X)
U3_ggg(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_ggg(X, Y, R)
U3_gag(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_ga(X, Y))
geq_in_ga(s(X), s(Y)) → U7_ga(X, Y, geq_in_ga(X, Y))
geq_in_ga(X, 0) → geq_out_ga(X, 0)
U7_ga(X, Y, geq_out_ga(X, Y)) → geq_out_ga(s(X), s(Y))
U5_gag(X, Y, geq_out_ga(X, Y)) → rem_out_gag(X, Y, X)
REM_IN_GAG(X, Y, R) → U1_GAG(X, Y, R, notZero_in_a(Y))
REM_IN_GAG(X, Y, R) → NOTZERO_IN_A(Y)
U1_GAG(X, Y, R, notZero_out_a(Y)) → U2_GAG(X, Y, R, sub_in_gaa(X, Y, Z))
U1_GAG(X, Y, R, notZero_out_a(Y)) → SUB_IN_GAA(X, Y, Z)
SUB_IN_GAA(s(X), s(Y), Z) → U6_GAA(X, Y, Z, sub_in_gaa(X, Y, Z))
SUB_IN_GAA(s(X), s(Y), Z) → SUB_IN_GAA(X, Y, Z)
U2_GAG(X, Y, R, sub_out_gaa(X, Y, Z)) → U3_GAG(X, Y, R, rem_in_ggg(Z, Y, R))
U2_GAG(X, Y, R, sub_out_gaa(X, Y, Z)) → REM_IN_GGG(Z, Y, R)
REM_IN_GGG(X, Y, R) → U1_GGG(X, Y, R, notZero_in_g(Y))
REM_IN_GGG(X, Y, R) → NOTZERO_IN_G(Y)
U1_GGG(X, Y, R, notZero_out_g(Y)) → U2_GGG(X, Y, R, sub_in_gga(X, Y, Z))
U1_GGG(X, Y, R, notZero_out_g(Y)) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, sub_in_gga(X, Y, Z))
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
U2_GGG(X, Y, R, sub_out_gga(X, Y, Z)) → U3_GGG(X, Y, R, rem_in_ggg(Z, Y, R))
U2_GGG(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGG(Z, Y, R)
REM_IN_GGG(X, Y, X) → U4_GGG(X, Y, notZero_in_g(Y))
REM_IN_GGG(X, Y, X) → NOTZERO_IN_G(Y)
U4_GGG(X, Y, notZero_out_g(Y)) → U5_GGG(X, Y, geq_in_gg(X, Y))
U4_GGG(X, Y, notZero_out_g(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → U7_GG(X, Y, geq_in_gg(X, Y))
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
REM_IN_GAG(X, Y, X) → U4_GAG(X, Y, notZero_in_a(Y))
REM_IN_GAG(X, Y, X) → NOTZERO_IN_A(Y)
U4_GAG(X, Y, notZero_out_a(Y)) → U5_GAG(X, Y, geq_in_ga(X, Y))
U4_GAG(X, Y, notZero_out_a(Y)) → GEQ_IN_GA(X, Y)
GEQ_IN_GA(s(X), s(Y)) → U7_GA(X, Y, geq_in_ga(X, Y))
GEQ_IN_GA(s(X), s(Y)) → GEQ_IN_GA(X, Y)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gaa(X, Y, Z))
sub_in_gaa(s(X), s(Y), Z) → U6_gaa(X, Y, Z, sub_in_gaa(X, Y, Z))
sub_in_gaa(X, 0, X) → sub_out_gaa(X, 0, X)
U6_gaa(X, Y, Z, sub_out_gaa(X, Y, Z)) → sub_out_gaa(s(X), s(Y), Z)
U2_gag(X, Y, R, sub_out_gaa(X, Y, Z)) → U3_gag(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, R) → U1_ggg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_ggg(X, Y, R, notZero_out_g(Y)) → U2_ggg(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_ggg(X, Y, R, sub_out_gga(X, Y, Z)) → U3_ggg(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, X) → U4_ggg(X, Y, notZero_in_g(Y))
U4_ggg(X, Y, notZero_out_g(Y)) → U5_ggg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_ggg(X, Y, geq_out_gg(X, Y)) → rem_out_ggg(X, Y, X)
U3_ggg(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_ggg(X, Y, R)
U3_gag(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_ga(X, Y))
geq_in_ga(s(X), s(Y)) → U7_ga(X, Y, geq_in_ga(X, Y))
geq_in_ga(X, 0) → geq_out_ga(X, 0)
U7_ga(X, Y, geq_out_ga(X, Y)) → geq_out_ga(s(X), s(Y))
U5_gag(X, Y, geq_out_ga(X, Y)) → rem_out_gag(X, Y, X)
GEQ_IN_GA(s(X), s(Y)) → GEQ_IN_GA(X, Y)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gaa(X, Y, Z))
sub_in_gaa(s(X), s(Y), Z) → U6_gaa(X, Y, Z, sub_in_gaa(X, Y, Z))
sub_in_gaa(X, 0, X) → sub_out_gaa(X, 0, X)
U6_gaa(X, Y, Z, sub_out_gaa(X, Y, Z)) → sub_out_gaa(s(X), s(Y), Z)
U2_gag(X, Y, R, sub_out_gaa(X, Y, Z)) → U3_gag(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, R) → U1_ggg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_ggg(X, Y, R, notZero_out_g(Y)) → U2_ggg(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_ggg(X, Y, R, sub_out_gga(X, Y, Z)) → U3_ggg(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, X) → U4_ggg(X, Y, notZero_in_g(Y))
U4_ggg(X, Y, notZero_out_g(Y)) → U5_ggg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_ggg(X, Y, geq_out_gg(X, Y)) → rem_out_ggg(X, Y, X)
U3_ggg(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_ggg(X, Y, R)
U3_gag(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_ga(X, Y))
geq_in_ga(s(X), s(Y)) → U7_ga(X, Y, geq_in_ga(X, Y))
geq_in_ga(X, 0) → geq_out_ga(X, 0)
U7_ga(X, Y, geq_out_ga(X, Y)) → geq_out_ga(s(X), s(Y))
U5_gag(X, Y, geq_out_ga(X, Y)) → rem_out_gag(X, Y, X)
GEQ_IN_GA(s(X), s(Y)) → GEQ_IN_GA(X, Y)
GEQ_IN_GA(s(X)) → GEQ_IN_GA(X)
From the DPs we obtained the following set of size-change graphs:
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gaa(X, Y, Z))
sub_in_gaa(s(X), s(Y), Z) → U6_gaa(X, Y, Z, sub_in_gaa(X, Y, Z))
sub_in_gaa(X, 0, X) → sub_out_gaa(X, 0, X)
U6_gaa(X, Y, Z, sub_out_gaa(X, Y, Z)) → sub_out_gaa(s(X), s(Y), Z)
U2_gag(X, Y, R, sub_out_gaa(X, Y, Z)) → U3_gag(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, R) → U1_ggg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_ggg(X, Y, R, notZero_out_g(Y)) → U2_ggg(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_ggg(X, Y, R, sub_out_gga(X, Y, Z)) → U3_ggg(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, X) → U4_ggg(X, Y, notZero_in_g(Y))
U4_ggg(X, Y, notZero_out_g(Y)) → U5_ggg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_ggg(X, Y, geq_out_gg(X, Y)) → rem_out_ggg(X, Y, X)
U3_ggg(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_ggg(X, Y, R)
U3_gag(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_ga(X, Y))
geq_in_ga(s(X), s(Y)) → U7_ga(X, Y, geq_in_ga(X, Y))
geq_in_ga(X, 0) → geq_out_ga(X, 0)
U7_ga(X, Y, geq_out_ga(X, Y)) → geq_out_ga(s(X), s(Y))
U5_gag(X, Y, geq_out_ga(X, Y)) → rem_out_gag(X, Y, X)
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
From the DPs we obtained the following set of size-change graphs:
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gaa(X, Y, Z))
sub_in_gaa(s(X), s(Y), Z) → U6_gaa(X, Y, Z, sub_in_gaa(X, Y, Z))
sub_in_gaa(X, 0, X) → sub_out_gaa(X, 0, X)
U6_gaa(X, Y, Z, sub_out_gaa(X, Y, Z)) → sub_out_gaa(s(X), s(Y), Z)
U2_gag(X, Y, R, sub_out_gaa(X, Y, Z)) → U3_gag(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, R) → U1_ggg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_ggg(X, Y, R, notZero_out_g(Y)) → U2_ggg(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_ggg(X, Y, R, sub_out_gga(X, Y, Z)) → U3_ggg(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, X) → U4_ggg(X, Y, notZero_in_g(Y))
U4_ggg(X, Y, notZero_out_g(Y)) → U5_ggg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_ggg(X, Y, geq_out_gg(X, Y)) → rem_out_ggg(X, Y, X)
U3_ggg(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_ggg(X, Y, R)
U3_gag(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_ga(X, Y))
geq_in_ga(s(X), s(Y)) → U7_ga(X, Y, geq_in_ga(X, Y))
geq_in_ga(X, 0) → geq_out_ga(X, 0)
U7_ga(X, Y, geq_out_ga(X, Y)) → geq_out_ga(s(X), s(Y))
U5_gag(X, Y, geq_out_ga(X, Y)) → rem_out_gag(X, Y, X)
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y)) → SUB_IN_GGA(X, Y)
From the DPs we obtained the following set of size-change graphs:
U1_GGG(X, Y, R, notZero_out_g(Y)) → U2_GGG(X, Y, R, sub_in_gga(X, Y, Z))
U2_GGG(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGG(Z, Y, R)
REM_IN_GGG(X, Y, R) → U1_GGG(X, Y, R, notZero_in_g(Y))
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gaa(X, Y, Z))
sub_in_gaa(s(X), s(Y), Z) → U6_gaa(X, Y, Z, sub_in_gaa(X, Y, Z))
sub_in_gaa(X, 0, X) → sub_out_gaa(X, 0, X)
U6_gaa(X, Y, Z, sub_out_gaa(X, Y, Z)) → sub_out_gaa(s(X), s(Y), Z)
U2_gag(X, Y, R, sub_out_gaa(X, Y, Z)) → U3_gag(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, R) → U1_ggg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_ggg(X, Y, R, notZero_out_g(Y)) → U2_ggg(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_ggg(X, Y, R, sub_out_gga(X, Y, Z)) → U3_ggg(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, X) → U4_ggg(X, Y, notZero_in_g(Y))
U4_ggg(X, Y, notZero_out_g(Y)) → U5_ggg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_ggg(X, Y, geq_out_gg(X, Y)) → rem_out_ggg(X, Y, X)
U3_ggg(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_ggg(X, Y, R)
U3_gag(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_ga(X, Y))
geq_in_ga(s(X), s(Y)) → U7_ga(X, Y, geq_in_ga(X, Y))
geq_in_ga(X, 0) → geq_out_ga(X, 0)
U7_ga(X, Y, geq_out_ga(X, Y)) → geq_out_ga(s(X), s(Y))
U5_gag(X, Y, geq_out_ga(X, Y)) → rem_out_gag(X, Y, X)
U1_GGG(X, Y, R, notZero_out_g(Y)) → U2_GGG(X, Y, R, sub_in_gga(X, Y, Z))
U2_GGG(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGG(Z, Y, R)
REM_IN_GGG(X, Y, R) → U1_GGG(X, Y, R, notZero_in_g(Y))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
notZero_in_g(s(X)) → notZero_out_g(s(X))
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U1_GGG(X, Y, R, notZero_out_g(Y)) → U2_GGG(X, Y, R, sub_in_gga(X, Y))
U2_GGG(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGG(Z, Y, R)
REM_IN_GGG(X, Y, R) → U1_GGG(X, Y, R, notZero_in_g(Y))
sub_in_gga(s(X), s(Y)) → U6_gga(X, Y, sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X, 0, X)
notZero_in_g(s(X)) → notZero_out_g(s(X))
U6_gga(X, Y, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(x0, x1)
notZero_in_g(x0)
U6_gga(x0, x1, x2)
REM_IN_GGG(y0, s(x0), y2) → U1_GGG(y0, s(x0), y2, notZero_out_g(s(x0)))
U1_GGG(X, Y, R, notZero_out_g(Y)) → U2_GGG(X, Y, R, sub_in_gga(X, Y))
U2_GGG(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGG(Z, Y, R)
REM_IN_GGG(y0, s(x0), y2) → U1_GGG(y0, s(x0), y2, notZero_out_g(s(x0)))
sub_in_gga(s(X), s(Y)) → U6_gga(X, Y, sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X, 0, X)
notZero_in_g(s(X)) → notZero_out_g(s(X))
U6_gga(X, Y, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(x0, x1)
notZero_in_g(x0)
U6_gga(x0, x1, x2)
U1_GGG(X, Y, R, notZero_out_g(Y)) → U2_GGG(X, Y, R, sub_in_gga(X, Y))
U2_GGG(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGG(Z, Y, R)
REM_IN_GGG(y0, s(x0), y2) → U1_GGG(y0, s(x0), y2, notZero_out_g(s(x0)))
sub_in_gga(s(X), s(Y)) → U6_gga(X, Y, sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X, 0, X)
U6_gga(X, Y, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(x0, x1)
notZero_in_g(x0)
U6_gga(x0, x1, x2)
notZero_in_g(x0)
U1_GGG(X, Y, R, notZero_out_g(Y)) → U2_GGG(X, Y, R, sub_in_gga(X, Y))
U2_GGG(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGG(Z, Y, R)
REM_IN_GGG(y0, s(x0), y2) → U1_GGG(y0, s(x0), y2, notZero_out_g(s(x0)))
sub_in_gga(s(X), s(Y)) → U6_gga(X, Y, sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X, 0, X)
U6_gga(X, Y, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(x0, x1)
U6_gga(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
REM_IN_GGG(y0, s(x0), y2) → U1_GGG(y0, s(x0), y2, notZero_out_g(s(x0)))
POL(0) = 0
POL(REM_IN_GGG(x1, x2, x3)) = 1 + x1 + x2
POL(U1_GGG(x1, x2, x3, x4)) = 1 + x1
POL(U2_GGG(x1, x2, x3, x4)) = x4
POL(U6_gga(x1, x2, x3)) = 1 + x3
POL(notZero_out_g(x1)) = 0
POL(s(x1)) = 1 + x1
POL(sub_in_gga(x1, x2)) = 1 + x1
POL(sub_out_gga(x1, x2, x3)) = 1 + x2 + x3
sub_in_gga(s(X), s(Y)) → U6_gga(X, Y, sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X, 0, X)
U6_gga(X, Y, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U1_GGG(X, Y, R, notZero_out_g(Y)) → U2_GGG(X, Y, R, sub_in_gga(X, Y))
U2_GGG(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGG(Z, Y, R)
sub_in_gga(s(X), s(Y)) → U6_gga(X, Y, sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X, 0, X)
U6_gga(X, Y, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
sub_in_gga(x0, x1)
U6_gga(x0, x1, x2)
SUB_IN_GAA(s(X), s(Y), Z) → SUB_IN_GAA(X, Y, Z)
rem_in_gag(X, Y, R) → U1_gag(X, Y, R, notZero_in_a(Y))
notZero_in_a(s(X)) → notZero_out_a(s(X))
U1_gag(X, Y, R, notZero_out_a(Y)) → U2_gag(X, Y, R, sub_in_gaa(X, Y, Z))
sub_in_gaa(s(X), s(Y), Z) → U6_gaa(X, Y, Z, sub_in_gaa(X, Y, Z))
sub_in_gaa(X, 0, X) → sub_out_gaa(X, 0, X)
U6_gaa(X, Y, Z, sub_out_gaa(X, Y, Z)) → sub_out_gaa(s(X), s(Y), Z)
U2_gag(X, Y, R, sub_out_gaa(X, Y, Z)) → U3_gag(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, R) → U1_ggg(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_ggg(X, Y, R, notZero_out_g(Y)) → U2_ggg(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_ggg(X, Y, R, sub_out_gga(X, Y, Z)) → U3_ggg(X, Y, R, rem_in_ggg(Z, Y, R))
rem_in_ggg(X, Y, X) → U4_ggg(X, Y, notZero_in_g(Y))
U4_ggg(X, Y, notZero_out_g(Y)) → U5_ggg(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_ggg(X, Y, geq_out_gg(X, Y)) → rem_out_ggg(X, Y, X)
U3_ggg(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_ggg(X, Y, R)
U3_gag(X, Y, R, rem_out_ggg(Z, Y, R)) → rem_out_gag(X, Y, R)
rem_in_gag(X, Y, X) → U4_gag(X, Y, notZero_in_a(Y))
U4_gag(X, Y, notZero_out_a(Y)) → U5_gag(X, Y, geq_in_ga(X, Y))
geq_in_ga(s(X), s(Y)) → U7_ga(X, Y, geq_in_ga(X, Y))
geq_in_ga(X, 0) → geq_out_ga(X, 0)
U7_ga(X, Y, geq_out_ga(X, Y)) → geq_out_ga(s(X), s(Y))
U5_gag(X, Y, geq_out_ga(X, Y)) → rem_out_gag(X, Y, X)
SUB_IN_GAA(s(X), s(Y), Z) → SUB_IN_GAA(X, Y, Z)
SUB_IN_GAA(s(X)) → SUB_IN_GAA(X)
From the DPs we obtained the following set of size-change graphs: